package typechecker;


import java.io.IOException;
import java.util.HashSet;
import java.util.Map;

import org.antlr.runtime.ANTLRFileStream;
import org.antlr.runtime.CommonTokenStream;
import org.antlr.runtime.RecognitionException;
import org.antlr.runtime.tree.CommonTree;
import org.antlr.runtime.tree.CommonTreeNodeStream;

import parser.TBTLexer;
import parser.TBTParser;
import typechecker.ast.ASTBuilder;
import typechecker.ast.Context;
import typechecker.ast.InductiveDatatype;
import typechecker.ast.term.DataConstructor;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;


public class TypeCheckerMain {
	
	public static boolean typecheck(String filename){
	    TBTLexer lex = null;
        CommonTree t = null;
		
        // Split the file into lexical atoms
        try {
        	lex = new TBTLexer(new ANTLRFileStream(filename, "UTF8"));
        } catch (IOException e1) {
			System.out.println("LEXICAL ERROR: " + e1.getMessage());
		}
        
        // Parse and obatin the Syntax Tree
        CommonTokenStream cts = new CommonTokenStream(lex);
        TBTParser g = new TBTParser(cts);
		try {
			t = (CommonTree) g.program().getTree();
		} catch (RecognitionException e1) {
			System.out.println("SYNTAX ERROR: " + e1.getMessage());
		}
		
		// Build the Abstract Syntax Tree
        CommonTreeNodeStream cnts = new CommonTreeNodeStream(t);
        ASTBuilder astb = new ASTBuilder(cnts);
        ASTBuilder.prog_return ret = null;
        TypingContext tc = new TypingContext();
        try {
        	ret = astb.prog();
		} catch (RecognitionException e) {
			e.printStackTrace();
		}
		
		/* Type Checking */
		
		// Build the initial environment containing the type constructors and check them 
		for( InductiveDatatype idt : ret.rdts){ 
    		idt.checkAndAnnotateDef();
    		for( Map.Entry<DataConstructor, TypeExpression> cons : idt.entrySet()){
    			tc.put(cons.getKey(), cons.getValue());
    		}
    	}
    	
		/* Infer the type of the main program doing all the checks along the way */
		ConstraintGraph c = new ConstraintGraph();
		TypeExpression theType = null;
		try{
			theType = new InferType().infer(ret.exp, c, new HashSet<Integer>(), tc, new Context<TypeVariable>() );
		} catch (TypeCheckingException tex){
			System.out.println("TYPE ERROR : " + tex.getMessage());
			return false;
		}
		
		if(InferType.errors == 0){
			System.out.println("type = "+ theType.preetyPrint());
			System.out.println(c.preetyPrint());
		} else {
			System.out.println(""+ InferType.errors + " type error(s)");
			return false;
		}
    	// XXX output dot file
		return true;
	}
	public static void main(String args[]) throws TypeCheckingException{
    	
//		typecheck("D:\\workspace\\TBT-front-end\\test\\parser.tbt");
//		typecheck("D:\\workspace\\TBT-front-end\\test\\dict.tbt");
		typecheck("D:\\workspace\\TBT-front-end\\test\\prelude.tbt");
    	
		
		
	}
}
 